$\forall$$p$:IdLnk List, $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$p$$\parallel$}}$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$i$+1}}$. \\[0ex]lpath($p$) $\Rightarrow$ lconnects(l\_interval($p$;$j$;$i$);source($p$[$j$]);source($p$[$i$]))